﻿using System;
using ParserGenerator.Collections;
using ParserGenerator.DataStructures;
using ParserGenerator.Extensions;
using ParserGenerator.Exceptions;
using ParserGenerator.Output;
using System.Numerics;

namespace ParserGenerator.Languages.LocalTypeInference
{
    partial class SyntaxTreeNodeWriter
    {
        public virtual void WriteIdentifier(Identifier n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            if (LocalTypeInferenceProgramParser.IsKeyword(n.Name))
                writer.Write("@");
            writer.Write(n.Name);
        }

        public virtual void WriteIntLiteral(IntLiteral n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write(n.Value);
        }

        public virtual void WriteParameter(Parameter n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteIdentifier(n.Name, writer);
            writer.Write(": ");
            WriteType(n.Type, writer);
        }

        public virtual void WriteParameterList(ParameterList n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            for (int i = 0; i < n.Items.Count; i++)
            {
                if (i > 0)
                    writer.Write(", ");
                WriteParameter(n.Items[i], writer);
            }
        }

        public virtual void WriteArgumentList(ArgumentList n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            for (int i = 0; i < n.Items.Count; i++)
            {
                if (i > 0)
                    writer.Write(", ");
                WriteExpression(n.Items[i], writer);
            }
        }

        public virtual void WriteTypeParameter(TypeParameter n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteIdentifier(n.Name, writer);
        }

        public virtual void WriteTypeParameterList(TypeParameterList n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            for (int i = 0; i < n.Items.Count; i++)
            {
                if (i > 0)
                    writer.Write(", ");
                WriteTypeParameter(n.Items[i], writer);
            }
        }

        public virtual void WriteTypeArgumentList(TypeArgumentList n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            for (int i = 0; i < n.Items.Count; i++)
            {
                if (i > 0)
                    writer.Write(", ");
                WriteType(n.Items[i], writer);
            }
        }

        public virtual void WriteVariableExpression(VariableExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteIdentifier(n.Name, writer);
        }

        public virtual void WriteFalseExpression(FalseExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("false");
        }

        public virtual void WriteTrueExpression(TrueExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("true");
        }

        public virtual void WriteIntLiteralExpression(IntLiteralExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteIntLiteral(n.Value, writer);
        }

        public virtual void WriteGroupExpression(GroupExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("(");
            WriteExpression(n.Operand, writer);
            writer.Write(")");
        }

        public virtual void WriteUnaryExpression(UnaryExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteUnaryOp(n.Op, writer);
            WriteExpression(n.Operand, writer);
        }

        public virtual void WriteBinaryExpression(BinaryExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteExpression(n.Left, writer);
            writer.Write(" ");
            WriteBinaryOp(n.Op, writer);
            writer.Write(" ");
            WriteExpression(n.Right, writer);
        }

        public virtual void WriteFunctionExpression(FunctionExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            using (writer.ColumnAlignment)
            {
                writer.Write("def ");
                if (n.TypeParameters != null)
                {
                    writer.Write("[");
                    WriteTypeParameterList(n.TypeParameters, writer);
                    writer.Write("]");
                }
                writer.Write("(");
                WriteParameterList(n.Parameters, writer);
                writer.Write(")");
                writer.Write("\n");
                writer.OpenCurlyBlock();
                WriteExpression(n.Body, writer);
                writer.Write("\n");
                writer.CloseCurlyBlock();
            }
        }

        public virtual void WriteCallExpression(CallExpression n, IndentedWriter writer, int d)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteExpression(n.Function, writer);
            if (n.TypeArguments != null)
            {
                writer.Write("[");
                WriteTypeArgumentList(n.TypeArguments, writer);
                writer.Write("]");
            }
            writer.Write("(");
            WriteArgumentList(n.Arguments, writer);
            writer.Write(")");
        }

        public virtual void WritePositiveUnaryOp(PositiveUnaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("+");
        }

        public virtual void WriteNegativeUnaryOp(NegativeUnaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("-");
        }

        public virtual void WriteLogicalNotUnaryOp(LogicalNotUnaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("!");
        }

        public virtual void WriteAddBinaryOp(AddBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("+");
        }

        public virtual void WriteSubtractBinaryOp(SubtractBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("-");
        }

        public virtual void WriteMultiplyBinaryOp(MultiplyBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("*");
        }

        public virtual void WriteDivideBinaryOp(DivideBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("/");
        }

        public virtual void WriteModuloBinaryOp(ModuloBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("%");
        }

        public virtual void WriteEqualToBinaryOp(EqualToBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("==");
        }

        public virtual void WriteNotEqualToBinaryOp(NotEqualToBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("!=");
        }

        public virtual void WriteLessThanBinaryOp(LessThanBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("<");
        }

        public virtual void WriteLessEqualBinaryOp(LessEqualBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("<=");
        }

        public virtual void WriteGreaterThanBinaryOp(GreaterThanBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write(">");
        }

        public virtual void WriteGreaterEqualBinaryOp(GreaterEqualBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write(">=");
        }

        public virtual void WriteLogicalAndBinaryOp(LogicalAndBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("&&");
        }

        public virtual void WriteLogicalOrBinaryOp(LogicalOrBinaryOp n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("||");
        }

        public virtual void WriteVariableType(VariableType n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteIdentifier(n.Name, writer);
        }

        public virtual void WriteObjectType(ObjectType n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("object");
        }

        public virtual void WriteNullType(NullType n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("null");
        }

        public virtual void WriteBoolType(BoolType n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("bool");
        }

        public virtual void WriteIntType(IntType n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            writer.Write("int");
        }

        public virtual void WriteFunctionType(FunctionType n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            if (n.TypeParameters != null)
            {
                writer.Write("forall ");
                WriteTypeParameterList(n.TypeParameters, writer);
                writer.Write(". ");
            }
            for (int i = 0; i < n.Sources.Count; i++)
            {
                if (i > 0)
                    writer.Write(" * ");
                if (n.Sources[i].IsFunction)
                    writer.Write("(");
                WriteType(n.Sources[i], writer);
                if (n.Sources[i].IsFunction)
                    writer.Write(")");
            }
            writer.Write(" -> ");
            if (n.Target.IsFunction)
                writer.Write("(");
            WriteType(n.Target, writer);
            if (n.Target.IsFunction)
                writer.Write(")");
        }

        public virtual void WriteValueVariableBinding(ValueVariableBinding n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteIdentifier(n.Name, writer);
            writer.Write(": ");
            WriteType(n.Type, writer);
        }

        public virtual void WriteTypeVariableBinding(TypeVariableBinding n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteIdentifier(n.Name, writer);
        }

        public virtual void WriteTypeSubstitutionVariableBinding(TypeSubstitutionVariableBinding n, IndentedWriter writer)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (writer == null)
                throw new ArgumentNullException(nameof(writer));
            WriteIdentifier(n.Name, writer);
            writer.Write(" => ");
            WriteType(n.Type, writer);
        }
    }

    partial class LocalTypeInferenceProgramParser
    {
        private void ScanIdentifierName()
        {
            string value = TokenContext.GetSource();
            TokenValue = Identifier.New(value, TokenContext);
        }

        private void ScanIntegerValue()
        {
            string str = TokenContext.GetSource();
            BigInteger v = BigInteger.Parse(str);
            TokenValue = IntLiteral.New(v, TokenContext);
        }
    }

    partial class LocalTypeInferenceTypeChecker
    {
        private static bool TypeParametersMatch(TypeParameterList x, TypeParameterList y)
        {
            if (x == null && y != null)
                return false;
            if (x != null && y == null)
                return false;
            if (x != null && y != null)
            {
                if (x.Items.Count != y.Items.Count)
                    return false;
                for (int i = 0; i < x.Items.Count; i++)
                    if (x.Items[i].Name.Name != y.Items[i].Name.Name)
                        return false;
            }
            return true;
        }

        private static bool TypeParametersMatch(FunctionType f, FunctionType g)
        {
            if (f == null)
                throw new ArgumentNullException(nameof(f));
            if (g == null)
                throw new ArgumentNullException(nameof(g));
            return TypeParametersMatch(f.TypeParameters, g.TypeParameters);
        }

        public static bool IsSubtypeOf(Type x, Type y)
        {
            if (x == null)
                throw new ArgumentNullException(nameof(x));
            if (y == null)
                throw new ArgumentNullException(nameof(y));
            if (x.IsVariable && y.IsVariable && x.AsVariable.Name.Name == y.AsVariable.Name.Name)
                return true;
            if (y.IsObject)
                return true;
            if (x.IsNull)
                return true;
            if (x.IsBool && y.IsBool)
                return true;
            if (x.IsInt && y.IsInt)
                return true;
            if (x.IsFunction && y.IsFunction)
            {
                var f = x.AsFunction;
                var g = y.AsFunction;
                if (f.Sources.Count != g.Sources.Count)
                    return false;
                if (!TypeParametersMatch(f, g))
                    return false;
                for (int i = 0; i < f.Sources.Count; i++)
                    if (!IsSubtypeOf(g.Sources[i], f.Sources[i]))
                        return false;
                return IsSubtypeOf(f.Target, g.Target);
            }
            return false;
        }

        public static Type JoinType(Type x, Type y)
        {
            if (x == null)
                throw new ArgumentNullException(nameof(x));
            if (y == null)
                throw new ArgumentNullException(nameof(y));
            if (x.IsObject)
                return x;
            if (y.IsObject)
                return y;
            if (x.IsNull)
                return y;
            if (y.IsNull)
                return x;
            if (x.IsVariable && y.IsVariable && x.AsVariable.Name.Name == y.AsVariable.Name.Name)
                return x;
            if (x.IsBool && y.IsBool)
                return x;
            if (x.IsInt && y.IsInt)
                return x;
            if (x.IsFunction && y.IsFunction)
            {
                var f = x.AsFunction;
                var g = y.AsFunction;
                if (f.Sources.Count != g.Sources.Count)
                    return Type.NewObject();
                if (!TypeParametersMatch(f, g))
                    return Type.NewObject();
                Sequence<Type> sources = Sequence.GetEmpty<Type>();
                for (int i = 0; i < f.Sources.Count; i++)
                {
                    Type source = MeetType(f.Sources[i], g.Sources[i]);
                    sources = Sequence.Append(sources, source);
                }
                Type target = JoinType(f.Target, g.Target);
                return Type.NewFunction(f.TypeParameters, sources, target);
            }
            return Type.NewObject();
        }

        public static Type MeetType(Type x, Type y)
        {
            if (x == null)
                throw new ArgumentNullException(nameof(x));
            if (y == null)
                throw new ArgumentNullException(nameof(y));
            if (x.IsObject)
                return y;
            if (y.IsObject)
                return x;
            if (x.IsNull)
                return x;
            if (y.IsNull)
                return y;
            if (x.IsVariable && y.IsVariable && x.AsVariable.Name.Name == y.AsVariable.Name.Name)
                return x;
            if (x.IsBool && y.IsBool)
                return x;
            if (x.IsInt && y.IsInt)
                return x;
            if (x.IsFunction && y.IsFunction)
            {
                var f = x.AsFunction;
                var g = y.AsFunction;
                if (f.Sources.Count != g.Sources.Count)
                    return Type.NewNull();
                if (!TypeParametersMatch(f, g))
                    return Type.NewNull();
                Sequence<Type> sources = Sequence.GetEmpty<Type>();
                for (int i = 0; i < f.Sources.Count; i++)
                {
                    Type source = JoinType(f.Sources[i], g.Sources[i]);
                    sources = Sequence.Append(sources, source);
                }
                Type target = MeetType(f.Target, g.Target);
                return Type.NewFunction(f.TypeParameters, sources, target);
            }
            return Type.NewNull();
        }

        private static Type SubstituteType(Type n, SymbolStack<string, VariableBinding> context)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (context == null)
                throw new ArgumentNullException(nameof(context));
            if (n.IsVariable)
            {
                VariableBinding binding = context.LookupValue(n.AsVariable.Name.Name);
                if (binding == null || binding.IsType)
                    return n;
                if (binding.IsTypeSubstitution)
                    return binding.AsTypeSubstitution.Type;
                string message = string.Format(SR.SymbolNotType, n.AsVariable.Name.Name.AsSingleQuote());
                TypeErrorException e = new TypeErrorException(message);
                e.AddLocation(n.Context);
                throw e;
            }
            if (n.IsFunction)
            {
                var f = n.AsFunction;
                if (f.TypeParameters != null)
                    foreach (TypeParameter tparam in f.TypeParameters.Items)
                        context.Push(tparam.Name.Name, VariableBinding.NewType(tparam.Name));
                Sequence<Type> sources = f.Sources.Map(x => SubstituteType(x, context));
                Type target = SubstituteType(f.Target, context);
                if (f.TypeParameters != null)
                    context.Pop(f.TypeParameters.Items.Count);
                return Type.NewFunction(f.TypeParameters, sources, target);
            }
            return n;
        }

        public static Type TypeCheck(Expression n)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            var context = new SymbolStack<string, VariableBinding>();
            return TypeCheck(n, context);
        }

        public static Type TypeCheck(Expression n, SymbolStack<string, VariableBinding> context)
        {
            if (n == null)
                throw new ArgumentNullException(nameof(n));
            if (context == null)
                throw new ArgumentNullException(nameof(context));
            if (n.IsVariable)
            {
                VariableBinding binding = context.FindValue(n.AsVariable.Name.Name, n.Context);
                if (!binding.IsValue)
                {
                    string message = string.Format(SR.SymbolNotValue, n.AsVariable.Name.Name.AsSingleQuote());
                    TypeErrorException e = new TypeErrorException(message);
                    e.AddLocation(n.Context);
                    throw e;
                }
                return binding.AsValue.Type;
            }
            if (n.IsFalse)
                return Type.NewBool();
            if (n.IsTrue)
                return Type.NewBool();
            if (n.IsIntLiteral)
                return Type.NewInt();
            if (n.IsUnary)
            {
                Type t = TypeCheck(n.AsUnary.Operand, context);
                switch (n.AsUnary.Op.Tag)
                {
                    case UnaryOpCategory.Positive:
                    case UnaryOpCategory.Negative:
                        if (!t.IsInt)
                        {
                            string message = string.Format(SR.IntValueExpected, t);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsUnary.Operand.Context);
                            throw e;
                        }
                        return t;
                    default:
                        if (!t.IsBool)
                        {
                            string message = string.Format(SR.BoolValueExpected, t);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsUnary.Operand.Context);
                            throw e;
                        }
                        return t;
                }
            }
            if (n.IsBinary)
            {
                Type t = TypeCheck(n.AsBinary.Left, context);
                Type t2 = TypeCheck(n.AsBinary.Right, context);
                switch (n.AsBinary.Op.Tag)
                {
                    case BinaryOpCategory.Add:
                    case BinaryOpCategory.Subtract:
                    case BinaryOpCategory.Multiply:
                    case BinaryOpCategory.Divide:
                    case BinaryOpCategory.Modulo:
                        if (!t.IsInt)
                        {
                            string message = string.Format(SR.IntValueExpected, t);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Left.Context);
                            throw e;
                        }
                        if (!t2.IsInt)
                        {
                            string message = string.Format(SR.IntValueExpected, t2);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Right.Context);
                            throw e;
                        }
                        return t;
                    case BinaryOpCategory.EqualTo:
                    case BinaryOpCategory.NotEqualTo:
                        if (!t.IsInt && !t.IsBool)
                        {
                            string message = string.Format(SR.IntOrBoolValueExpected, t);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Left.Context);
                            throw e;
                        }
                        if (!t2.IsInt && !t2.IsBool)
                        {
                            string message = string.Format(SR.IntOrBoolValueExpected, t2);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Right.Context);
                            throw e;
                        }
                        if (t.Tag != t2.Tag)
                        {
                            string message = string.Format(SR.OperandTypesMismatch, t, t2);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Left.Context);
                            e.AddLocation(n.AsBinary.Right.Context);
                            throw e;
                        }
                        return Type.NewBool();
                    case BinaryOpCategory.LessThan:
                    case BinaryOpCategory.LessEqual:
                    case BinaryOpCategory.GreaterThan:
                    case BinaryOpCategory.GreaterEqual:
                        if (!t.IsInt)
                        {
                            string message = string.Format(SR.IntValueExpected, t);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Left.Context);
                            throw e;
                        }
                        if (!t2.IsInt)
                        {
                            string message = string.Format(SR.IntValueExpected, t2);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Right.Context);
                            throw e;
                        }
                        return Type.NewBool();
                    default:
                        if (!t.IsBool)
                        {
                            string message = string.Format(SR.BoolValueExpected, t);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Left.Context);
                            throw e;
                        }
                        if (!t2.IsBool)
                        {
                            string message = string.Format(SR.BoolValueExpected, t2);
                            TypeErrorException e = new TypeErrorException(message);
                            e.AddLocation(n.AsBinary.Right.Context);
                            throw e;
                        }
                        return t;
                }
            }
            if (n.IsFunction)
            {
                var f = n.AsFunction;
                if (f.TypeParameters != null)
                    foreach (TypeParameter tparam in f.TypeParameters.Items)
                        context.Push(tparam.Name.Name, VariableBinding.NewType(tparam.Name));
                foreach (Parameter param in f.Parameters)
                    context.Push(param.Name.Name, VariableBinding.NewValue(param.Name, param.Type));
                Type target = TypeCheck(f.Body, context);
                context.Pop(f.Parameters.Items.Count);
                if (f.TypeParameters != null)
                    context.Pop(f.TypeParameters.Items.Count);
                Sequence<Type> sources = f.Parameters.Items.Map(x => x.Type);
                return Type.NewFunction(f.TypeParameters, sources, target);
            }
            if (n.IsCall)
            {
                var c = n.AsCall;
                Type fType = TypeCheck(c.Function, context);
                Sequence<Type> argTypes = c.Arguments.Items.Map(x => TypeCheck(x, context));
                if (fType.IsNull)
                    return fType;
                if (!fType.IsFunction)
                {
                    TypeErrorException e = new TypeErrorException(SR.FunctionExpectedHere);
                    e.AddLocation(c.Function.Context);
                    throw e;
                }
                var f = fType.AsFunction;
                int typeArgumentCount = c.TypeArguments?.Items.Count ?? 0;
                int fTypeParameterCount = f.TypeParameters?.Items.Count ?? 0;
                if (typeArgumentCount != fTypeParameterCount)
                {
                    string message = string.Format(SR.TypeParameterAndArgumentCountMismatch, fTypeParameterCount, typeArgumentCount);
                    TypeErrorException e = new TypeErrorException(message);
                    e.AddLocation(c.Function.Context);
                    throw e;
                }
                int argumentCount = c.Arguments.Items.Count;
                int fParameterCount = f.Sources.Count;
                if (argumentCount != fParameterCount)
                {
                    string message = string.Format(SR.FunctionParameterAndArgumentCountMismatch, fParameterCount, argumentCount);
                    TypeErrorException e = new TypeErrorException(message);
                    e.AddLocation(c.Function.Context);
                    throw e;
                }
                if (fTypeParameterCount > 0)
                {
                    for (int i = 0; i < fTypeParameterCount; i++)
                    {
                        TypeParameter tparam = f.TypeParameters.Items[i];
                        Type targ = c.TypeArguments.Items[i];
                        context.Push(tparam.Name.Name, VariableBinding.NewTypeSubstitution(tparam.Name, targ));
                    }
                }
                Sequence<Type> paramTypes = f.Sources.Map(x => SubstituteType(x, context));
                for (int i = 0; i < argumentCount; i++)
                {
                    Type argType = argTypes[i];
                    Type paramType = paramTypes[i];
                    if (!IsSubtypeOf(argType, paramType))
                    {
                        string message = string.Format(SR.ArgumentMustBeOfTypeOrSubtypeOf, i + 1, paramType, argType);
                        TypeErrorException e = new TypeErrorException(message);
                        e.AddLocation(c.Arguments.Items[i].Context);
                        throw e;
                    }
                }
                Type resultType = SubstituteType(f.Target, context);
                if (fTypeParameterCount > 0)
                    context.Pop(fTypeParameterCount);
                return resultType;
            }
            NotImplementedErrorException ex = new NotImplementedErrorException(SR.TypeCheckingNotImplemented);
            ex.AddLocation(n.Context);
            throw ex;
        }
    }
}
